Before computers, mathematicians used to define functions by
recursion.  It turns out that a small modification of old-fashioned
recursion equations gives a language with assignment statements and
conditional {\bfgo to}s.  The advantage is that properties of the
programs are consequences of the recursion equations themselves,
together with a theory of the data domain, without any special theory of
programming.  The idea was previously explored by Francez (197x) and
Pnueli (197x), but they mistakenly abandoned it for temporal logic.
The purpose of this paper is to resurrect it with some important
variations.

	Consider the Algol program fragment

start:	p := 0;
	i := n;
loop:	if i = 0 then go to done;
	p := p + m;
	i := i - 1;
	go to loop;
done:

\noindent The data are assumed to be natural numbers.  If the program
starts at the label $start$, it clearly  reaches the label $done$ with
$p$  having the value $m*n$.  This can be proved formally using the
Floyd method of inductive assertions or the Hoare axioms, although
these formalisms require a separate proof of termination.

	The corresponding Algol 50 program is

$$∀t m n.\xi(t+1) = \if pc(\xi(t)) = start \then step(a(p,0,\xi(t)))
\elseif pc(\xi(t)) = start+1 \then step(a(i,n,\xi(t)))
\elseif pc(\xi(t)) = start+2 \then
		(if c(i,\xi(t)) = 0 \then goto(done,\xi(t))
				\else step(\xi(t)))
\elseif pc(\xi(t)) = start+3 \then step(a(p,c(p,\xi(t)) + m,\xi(t)))
\elseif pc(\xi(t)) = start+4 \then step(a(i,c(p,\xi(t)) - 1,\xi(t)))
\elseif pc(\xi(t)) = start+5 \then goto(loop,\xi(t)),$$
%
\noindent where
%
$$done = start+6$$
%
\noindent and
%
$$loop = start+2.$$

	In the above we use the abbreviations
%
$$∀l \xi.goto(l,\xi) = a(pc,l,\xi),$$
%
$$∀\xi.step(\xi) = a(pc,pc(\xi)+1,\xi),$$
%
$$∀\xi.pc(\xi) = c(pc,\xi).$$